Definitions are introduced for polymorphic identity and
composition functions, and for predicates such as
injectivity and surjectivity.
Basic properties of the functions are proven, as are
inter-relationshsips between the predicates.
Variatns on lambda abstraction and the identity function are
introduced that include type tags that vanish when the definitions
are unfolded. Use of these type tags is encouraged, since the
type inference routines sometimes have difficulties without them
(the current type inference routine works on terms bottom up, and
doesn't handle polymorhic types as well as it should).